| Definitions | t  T,  b,  A,  b,  , s = t, Prop, Rplus?(x1), x:A  B(x), x:A B(x), P & Q, P   Q, Unit, left+right,   , {x:A| B(x) }, #$n, a<b, Void, False,  , i j, -n, n-m, R-size(R), n+m, R-icompat(A;B), R-interface(A;B), P  Q, R-Feasible(R), A B, Realizer,  x:A. B(x), , Rplus-right(x1), Rplus-left(x1), {T}, Id, Knd, Type, f || g, R-loc(R), a = b, R-interface-compat(A;B), if b t else f fi, True, Rnone?(x1), Rsends?(x1), @loc: only members of L read x, Top, rcv(l,tg), KindDeq, destination(l), R-da(R;i),  x.A(x), x. t(x), f(x)?z, IdLnk, source(l), es realizer ind Rrframe compseq tag def, Atom$n, rec(x.A(x)), type List, es realizer ind, A & B, Rsends-dt(x1), Rsends-l(x1), Rsends-T(x1), Rsends-knd(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), @loc: k sends only on links in L, es realizer ind Rbframe compseq tag def, @loc: k writes only members of L, es realizer ind Raframe compseq tag def, locl(a), x : v, @loc precondition for a(v:T):P State(ds) v, EqDecider(T), a:A fp B(a), , es realizer ind Rpre compseq tag def, let x = a in b(x), sends knd(v:T) on l:tagged(g,State(ds),v):dt, lnk-decl(l;dt), f  g, es realizer ind Rsends compseq tag def, Case b of inl(x) s(x) ; inr(y) t(y), @loc effect knd(v:T) x := f State(ds) v , es realizer ind Reffect compseq tag def, only events in L send on lnk with tag, es realizer ind Rsframe compseq tag def, @loc only events in L change x:T, es realizer ind Rframe compseq tag def, @loc x initially v:T, es realizer ind Rinit compseq tag def, left right, es realizer ind Rplus compseq tag def,  , es realizer ind Rnone compseq tag def, State(ds), DeclaredType(ds;x), lnk(k), isrcv(k), Normal(T), Normal(ds), xdom(f). v=f(x) P(x;v), f(a),  x:A. B(x), Dec(P), tag(k), IdDeq, AtomFree(T;x), A || B, , p  q, a = b, SQType(T), s ~ t, P  Q, <a,b>,  T,  x:A. B(x), x dom(f), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l) |
| Lemmas | fpf-cap-single-join, fpf-cap-single1, isrcv-implies, lnk-decl-cap, IdLnk sq, fpf-single-dom, Knd sq, fpf-join-cap-sq, fpf-trivial-subtype-top, fpf-dom wf, subtype rel wf, squash wf, bool cases, bool sq, assert-eq-lnk, eq lnk wf, it wf, R-compat wf, atom-free wf, id-deq wf, tagof wf, decidable wf, locl wf, normal-ds wf, normal-type wf, isrcv wf, lnk wf, unit wf, decl-type wf, decl-state wf, Rnone wf, true wf, Rplus wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, ifthenelse wf, fpf wf, fpf-join wf, lnk-decl wf, fpf-empty wf, Rsends wf, fpf-single wf, subtype rel self, deq wf, Rpre wf, Raframe wf, Rbframe wf, false wf, lsrc wf, IdLnk wf, fpf-cap wf, Knd wf, R-da wf, ldst wf, Kind-deq wf, rcv wf, top wf, Rrframe wf, Rsends? wf, Rnone? wf, not functionality wrt iff, assert-eq-id, eq id wf, R-loc wf, R-interface-Rplus2, R-interface-Rplus, Id wf, R-compat-da, R-size-decreases, Rplus-left wf, Rplus-right wf, ge wf, nat properties, nat wf, R-interface wf, R-Feasible wf, le wf, R-size wf, nat plus wf, es realizer wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, Rplus? wf, bool wf, bnot wf, not wf, assert wf, Rplus-Feasible |